/*
File:			assertions.sv
Description:  	Verify the correct sequencing of 
				commands and signals
Author:			Katerina Gleeson

module assertions(DDR_bus BUS, CK, CK_bar);
import params::*;
command ENUM;


sequence RASL2RASH;  //verify RAS fall and rise time
	@(posedge CK)
	$fell(BUS.RAS) ##tRAS $rose(BUS.RAS);
endsequence

sequence CASL2CASH;  //verify CAS fall and rise time
	@(posedge CK)
	$fell(BUS.CAS) ##tCL $rose(BUS.CAS);

sequence ACT2PRE; //verify tRAS time between ACT and following PRE
	@(posedge CK)
	(BUS.ENUM == ACT) ##tRAS (BUS.ENUM == PRE);
endsequence


//make sure that RAS falls once row is on line
sequence ADDR2RAS;  
	@(posedge CK)
	$changed(BUS.ADDRESS_LINE)|-> $fell(BUS.RAS);
endsequence

sequence ADDR2CAS;  //after row and ras, need column and CAS. can overlap
	@(posedge CK)
	(ADDR2RAS |-> $changed(BUS.ADDRESS_LINE)) ##tRCD $fell(BUS.CAS);
endsequence


sequence RAS2CAS;  //Verify that CAS falls tRCD after RAS.
	@(posedge CK)
	$fell(BUS.RAS) ##tRCD $fell(BUS.CAS);
endsequence

sequence READ2DATA;
	@(posedge CK)
	RAS2CAS ##(tCL+tAL) ($changed(data && BUS.DQ && BUS.OE));
endsequence

sequence BURST;
	@(posedge CK)
	$changed(BUS.DQ && data) [*tBURST] $isunknown(BUS.DQ && data);

sequence TESTREAD;   //verify that after read signal is sent, address info follows.
	@(posedge CK)
	(BUS.ENUM == RD) |-> $changed(BUS.ADDRESS_LINE);
endsequence

//verify no other activity to a bank until tRP after a PRE

//need RAS2READ. send WE signal HIGH. then after tOE valid data is sent. all within tRC



sequence RAS2WRITEDATA;
	@(posedge CK)
	$fell(BUS.RAS) ##tRAS ($changed(ADDRESS_LINE && $fell(BUS.CAS) &&		$fell(BUS.WE) && $changed(BUS.DQ));
endsequence



endsequence WRITE2DATA; //WL = AL + CWL
	@(posedge CK)
	(BUS.ENUM == WR && $changed(bus.ADDRESS_LINE)) ##(tAL + tCWL) $changed(DQ);
endsequence


sequence TESTACT;  //test activate sequence..
//After a row is opened with an ACTIVATE command, a READ or WRITE command may be issued to that row, subject to the tRCD specification. 
//other tests should pick up where this leaves off
	@(posedge CK)
	(BUS.ENUM == ACT) |-> ($changed(BUS.ADDRESS_LINE) ##[0:tRCD] ((BUS.ENUM == RD || BUS.ENUM == WR)));
endsequence


sequence TESTPRE;  //verify precharge time before activate is asserted
	@(posedge CK)
	(BUS.ENUM == PRE) ##tRP (BUS.ENUM == ACT);
endsequence















